-
Notifications
You must be signed in to change notification settings - Fork 43
CERT 8687 Realistic example #167
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: cli-beta
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This example is way better now and easier to me. Looks good to me.
Is this subsuming #166 or do we take both examples?
We want to keep both PRs. So this can be merged alongside version 8. I added a label. |
Assigning @johspaeth (or someone from his team) to complete and merge this Example. |
https://certora.atlassian.net/browse/CERT-8687
Note We need to adjust the example as the invariant is currently violated in both semantic versions.
@nd-certora let me know how to fix it.